Nuprl Lemma : m-sys-join_wf 0,22

AB:System. A || B  (A  B System 
latex


Definitionsx:AB(x), f(a), M1 || M2, ma-frame-compatible(A;B), P & Q, A ||+ B, x:AB(x), t  T, Feasible(M), P  Q, M1  M2, M1 ||decl M2, A || B, Id, Type, x:AB(x), x.A(x), {x:AB(x) }, MsgA, System, A  B
Lemmasm-sys-compatible wf, msystem wf, ma-join wf, Id wf, ma-feasible wf, ma-join-feasible

origin